COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	% use this file for experimental typsetting using th `boo' macros
C00003 00003		In this section we introduce the reader to the methods of proving
C00018 00004	\end{document}
C00019 00005	% anything can go here as tex won't read beyond the \end{document}
C00020 ENDMK
C⊗;
% use this file for experimental typsetting using th `boo' macros

%  \pagelayout{boo}
\input{boo.plo[b2,jmc]}
%  \documentstyle{boo,boo11}
\input{boo.sty[b2,jmc]}
\input{boo11.sty[b2,jmc]}

\input boomac.tex[b2,jmc]

\nofiles

\begin{document}

	In this section we introduce the reader to the methods of proving
properties of programs. Our approach will be rather informal, the main aim
being to illustrate the ideas and tools that we will develop later. The object
of our attention will be the program \mkop{append}. In particular we wish to
prove that our program \mkop{append} behaves in a manner consistent with its name.
We shall accomplish this by proving that it satisfies 
certain mathematical principles. The principles that we have chosen are

1. \mkop{append}[|NIL|,$x$] = $x$

2. \mkop{append}[$x$,|NIL|] = $x$

3. \mkop{append}[$x$,\mkop{append}[$y$,$z$]] = \mkop{append}[\mkop{append}[$x$,$y$],$z$]

	In these equations $x,y$ and $z$ stand for any lists, in other words these three
equations are supposed to hold regardless of which particular lists $x,y$ and $z$ are.
While these properties do not guarantee that our program \mkop{append} does
exactly what we want it to do they are certainly necessary. The algebraic nature
of these properties is perhaps made more perspicuous if we write them out using
the infix notation

1'. $|NIL| \qapp\ x$ = $x$

2'. $x \qapp\ |NIL|$ = $x$

3'. $x \qapp\ ( y \qapp\ z)$ = $(x \qapp\ y) \qapp\ z)$
 
Thus 1' tells us that |NIL| is the left identity of the operation \qapp, while 2'
tells us that it is also the right identity . The third equation tells us that
the \qapp\ operation is associative, and all three together tell us that the
collection of lists together with the operation \qapp\ form what mathematicians 
call a {\it semigroup with identity}. For the convenience of the reader we
repeat the definition of \mkop{append}

$$\edefun{append}{%
(DEFUN APPEND (U V)
  (COND ((NULL U) V) (T (CONS (CAR U) (APPEND (CDR U) V))) ))
}$$

$$u \qapp v \leftarrow \qif \qn u \qthen v \qelse \qa u \qcons [\qd u] \qapp v$$
Let us begin with 1'.

\noindent{\bf Proposition 1:}   \mkop{append}[|NIL|,$x$] = $x$

\noindent{\bf Proof:}  This is a very easy proof. Since by the definition of \mkop{append}
we have that
$$\mkop{append}[|NIL|,x]= \qif \qn |NIL| \qthen x \qelse \qa |NIL| \qcons \mkop{append}[\qd |NIL|,x]$$
but remember that $\qn |NIL|$ just abreviated |NIL| = |NIL|. So clearly
$\qn |NIL|$ is true. Consequently the value of the conditional is the value of the
then clause. Which in this case is just $x$. Therefore
$\mkop{append}[|NIL|,x] = x$
and the proof is complete.  Q.E.D

	Now suppose we try the same strategy to prove 2'
$$\mkop{append}[x,|NIL|]
= \qif \qn x \qthen |NIL| \qelse \qa x \qcons \mkop{append}[\qd x, |NIL|]$$
but there does not seem to be anyway that we can simplify the right hand side.
We could of course expand out \mkop{append}[\qd x,|NIL|], but that would seem
only to complicate matters.
One way to proceed is to split the proof into cases, if we assume that $x$ is |NIL|
then we can simplify  the right hand side,
conversely if we assumed  that $x$ was not |NIL| then we could also simplify it.
So let us see where that gets us.

\noindent{\bf Case 1} $x$ = |NIL| : Here we have
$$\vbox{\halign{\hfil$#$&$\>=#$\hfil\cr
\mkop{append}[|NIL|,x]& \mkop{append}[|NIL|,|NIL|]\cr
& \qif \qn |NIL| \qthen |NIL| \qelse \qa |NIL| \qcons \mkop{append}[\qd |NIL|,|NIL|]\cr
& |NIL|\cr
& x\cr
}}$$
which was what we desired, now for the non |NIL| case.

\noindent{\bf Case 2} $x$ is not |NIL| : In this case
$$\mkop{append}[x,|NIL|]=\qa x \qcons \mkop{append}[\qd x, |NIL|]$$
Here again there is very little that we can do directly to simplify
the right hand side. But this is where the crucial idea of the proof comes in.
Although the last line looks more complicated, there is an aspect of
it which is simpler. In $x \qapp\ |NIL|$ the program \mkop{append} has to
compute the result of appending a list $x$ onto |NIL|, whereas in
$\qa x \qcons \mkop{append}[\qd x, |NIL|]$  it only has to compute the result
of appending \qd$x$ onto |NIL|. In other words the length of the list that
\mkop{append} has to append onto |NIL| has decreased by one. So let us suppose
in addition to the fact that $x$ is not |NIL| that our program \mkop{append}
satisfies 2' for all lists $y$ of length less that of $x$.
So in particular we have that \mkop{append}[\qd $x$,|NIL|] = \qd $x$
thus
$$\vbox{\halign{\hfil$#$&$\>=#$\hfil\cr
\qa x \qcons \mkop{append}[\qd x,|NIL|] & \qa x \qcons \qd x\cr
& x\cr
}}$$
So assuming that $x$ is not |NIL| and that $y \qapp |NIL|$ = $y$ for any list $y$
of length less than that of $x$, we have shown that $x \qapp |NIL|$ = $x$.
It just so happens that this together with case one constitutes a proof of
2'.
To convince the reader of this we rewrite it as follows.

\noindent{\bf Proposition 2:}   \mkop{append}[$x$,|NIL|] = $x$

\noindent{\bf Proof}:  We have already shown that \mkop{append}[|NIL|,|NIL|] is |NIL| is case 1.
Consequently we know that if there is a list $y$ such that $y \qapp |NIL| \neq y$ then
the length of $y$ must be greater than zero. So	let us suppose that our proposition
is false. In other words there are lists that fail to satisfy the equation
$x \qapp\ |NIL|$ = $x$. Let suppose $y$ is one such list, and furthermore let us
assume that all lists of length less than that of $y$ do in fact satisfy the 
equation.
We can do this because the length of a list is a Natural number, and so if there are
lists that do not satisfy the equation then some of them must  have the smallest
possible length.
Thus 
$$\vbox{\halign{\hfil$#$&$\>=#$\hfil\cr
y \qapp |NIL| & \qif \qn y \qthen |NIL| \qelse \qa y \qcons [\qd y \qapp |NIL|]\cr
&\qa y \qcons [\qd y \qapp |NIL|]\cr
&\qa y \qcons \qd y\cr
& \omit since $\qd y \qapp |NIL| = \qd$ by our choice of y \hfil\cr
& y\cr
}}$$

But this means that $y$ does indeed satisfy 2' which is a contradiction. So our
supposition that there were lists that did not satisfy it was wrong. Thus our
proposition is proved.  Q.E.D

  	This proof was really designed to show that by proving  case 1 and
case 2 we actually established our desired result.  
We can state  this  as the following principle of induction. 

 If a property  P is such that 

1. P is true of the empty list |NIL|

2. If P is true for all lists of length less than that of $y$, then P is also true $y$.

Then every list has the property P

	We shall call this induction on the length of lists. It is a special case
of a powerful proof technique that we shall develop in this chapter. As another
example of its use we prove our third property of /append/.

\noindent{\bf Theorem 1:}   \mkop{append}[$x$,\mkop{append}[$y$,$z$]] = \mkop{append}[\mkop{append}[$x$,$y$],$z$]

\noindent{\bf Proof:} The proof shall be by induction on the length of $x$. The base case
being when $x$ is |NIL|, or in other words when $x$ is of length 0.

\noindent{\bf Case 1:} Here we have 
$$\vbox{\halign{\hfil$#$&$\>=#$\hfil\cr
 \mkop{append}[x,\mkop{append}[y,z]] &  \mkop{append}[|NIL|,\mkop{append}[y,z]]\cr
& \qif \qn |NIL| \qthen /append/[y,z] \qelse \qa |NIL| \qcons /append/[\qd |NIL|,/append/[y,z]]\cr
& /append/[y,z]\cr
& \omit since $\qn |NIL|$ is true \hfil\cr
& \mkop{append}[\mkop{append}[|NIL|,y],z]\cr
& \omit since $|NIL| \qapp y = y$ \hfil\cr
& \mkop{append}[\mkop{append}[x,y],z]\cr
& \omit since $x = |NIL|$ \hfil\cr
}}$$
which is the desired result. Now we must do the non |NIL| case, or as it is
more commonly known th induction case.

\noindent{\bf Case 2:} So let us assume that $x$ is not |NIL| and that the theorem is true
for all lists of length less $x$. In this case
$$\vbox{\halign{\hfil$#$&$\>=#$\hfil\cr
 \mkop{append}[x,\mkop{append}[y,z]] 
& \qif \qn x \qthen /append/[y,z] \qelse \qa x \qcons /append/[\qd x,/append/[y,z]]\cr
& \qa x \qcons /append/[\qd x, /append/[y,z]]\cr
& \omit since $x$ is not |NIL| \hfill\cr
& \qa x \qcons /append/[/append/[\qd x,y],z]\cr
& \omit since by induction hypothesis we have $\qd x \qapp ( y \qapp z) = (\qd x \qapp y) \qapp z$ \hfil\cr
}}$$
It is at this point that we need a lemma that will enable us to simplify this
last line.

\noindent{\bf Lemma:}  $ x \qcons /append/[y,z] = /append/[x \qcons y,z]$

\noindent leaving the proof of the lemma aside for the moment, we can use it to obtain
$$\vbox{\halign{\hfil$#$&$\>=#$\hfil\cr
\qa x \qcons /append/[/append/[\qd x,y],z] & /append/[ \qa x \qcons /append/[\qd x, y], z]\cr
& \omit by the lemma \hfil\cr
& /append/[/append/[\qa x \qcons \qd x, y],z]\cr
& \omit again by the lemma \hfil\cr
& /append/[/append/[x,y],z]\cr
& \omit since $\qa x \qcons \qd x = x$ \hfil\cr
}}$$
thus modulo a proof of our lemma, the theorem is proved. Q.E.D

We finish of this introductory section with a proof of our lemma.

\noindent{\bf Proof of Lemma:} Here we have
$$\vbox{\halign{\hfil$#$&$\>=#$\hfil\cr
/append/[x \qcons y, z] & \qif \qn [x \qcons y] \qthen z \qelse \qa[ x \qcons y] \qcons /append/[ \qd[x \qcons y],z]\cr
& \qa[ x \qcons y] \qcons /append/[ \qd[x \qcons y],z]\cr
& \omit because $\qnot \qn [x \qcons y]$\hfil\cr
& x \qcons /append/[y,z]\cr
&  \omit Since $\qa[x \qcons y] = x$ and $\qd[x \qcons y] = y$\hfil\cr
}}$$
Q.E.D
\end{document}
% anything can go here as tex won't read beyond the \end{document}